Loogle!

An improved search engine for Lean:

• https://loogle.lean-fro.org/
• https://github.com/nomeata/loogle

I haven’t used it yet but it looks promising. I personally don’t like the search on mathlib4_docs and find it very glitchy, slow, and cumbersome. Normally, I just use grep in VSCode instead, which is better but still very cumbersome and requires a lot of regex jujitsu. Hopefully this search is better and more useful. Looking forward to trying it out.